package ss.pku.jsa.type.inference;

import java.util.HashMap;
import java.util.HashSet;
import java.util.Iterator;
import java.util.List;
import java.util.Map;
import java.util.Set;
import java.util.SortedSet;
import java.util.Stack;
import java.util.TreeSet;
import java.util.Vector;

import org.eclipse.jdt.core.ICompilationUnit;
import org.eclipse.jdt.core.IJavaProject;
import org.eclipse.jdt.core.dom.IBinding;
import org.eclipse.jdt.core.dom.ITypeBinding;
import org.eclipse.jdt.core.dom.IVariableBinding;

import ss.pku.jsa.type.constraint.solver.Native;
import ss.pku.jsa.type.io.FieldQSig;


@SuppressWarnings({ "unchecked", "rawtypes" })
public class Analysis {
	public static boolean TEST = false;

	public String results = "";

	private Map<Object, QType> qTypeMap = new HashMap<Object, QType>();

	public Stack<ConstraintJob> constraintWorklist = new Stack<ConstraintJob>();

	public Stack<MergeJob> mergeWorklist = new Stack<MergeJob>();

	public Set<IJavaProject> projects = new HashSet<IJavaProject>();

	private Set<String> typesSeen = new HashSet<String>();

	private Stack<ICompilationUnit> typesToVisit = new Stack<ICompilationUnit>();

	Set<ICompilationUnit> originalSet = new HashSet<ICompilationUnit>();

	public Set<TypeKey> typesUsed = new HashSet<TypeKey>();

	public Set<MethodKey> methodsUsed = new HashSet<MethodKey>();

	public Set<FieldKey> fieldsUsed = new HashSet<FieldKey>();

	public Set<TypeKey> typesDeclared = new HashSet<TypeKey>();

	public Set<MethodKey> methodsDeclared = new HashSet<MethodKey>();

	public Set<FieldKey> fieldsDeclared = new HashSet<FieldKey>();

	public int locCount = 0;
	public int maxEnum;
	public int ffiNumAnnotations = 0;

	public int numOriginalClasses = 0;

	public int numOriginalMethods = 0;
	public int numOriginalVars = 0;

	public SortedSet<Declaration> declarations = new TreeSet<Declaration>();

	public Set<Qualifier> readonlyAnnotations = new HashSet<Qualifier>();

	public Set<Qualifier> readonlyTextualAnnotationsInferred = new HashSet<Qualifier>();
	public Set<Qualifier> readonlyTextualAnnotationsNotInferred = new HashSet<Qualifier>();
	private JavariResults javariResults;
	public Map<String, Map> processedTypes = new HashMap<String, Map>();

	public Map<FFIResults.JNIMethodName, MethodQType> nativeMethods = new HashMap<FFIResults.JNIMethodName, MethodQType>();

	private Map<Integer, Qualifier> qualifiers = new HashMap<Integer, Qualifier>();

	private Map<Integer, Location> locations = new HashMap<Integer, Location>();

	Map<String, Qualifier> constants = new HashMap<String, Qualifier>();

	public long QTypeCount = 0L;

	private Set<FieldKey> mutableSet = new HashSet<FieldKey>();

	private HashMap<Location, Qualifier> locationQualifiers = new HashMap();

	HashMap<TypeKey, Set<FieldKey>> typeFieldsMap = new HashMap();

	private Map<TypeKey, ClassQType> classQTypeMap = new HashMap();

	public Vector<ObjectQType> objectQTypes = new Vector();

	HashMap fieldLocations = new HashMap();

	HashMap objectFieldNodeLocations = new HashMap();

	public Set<TypeKey> fieldSensitiveTypes = new HashSet();

	public Set<FieldKey> fieldSensitiveFields = new HashSet();
	QualGate gateBlockJavari;
	QualGate gateJavariOnly;
	QualGate gateJavariBackwardOnly;
	QualGate gateForwardOnly;
	QualGate gateInternedOnly;
	Qualifier mutable = null;

	Qualifier readonly = null;

	Qualifier transparent = null;

	Qualifier qual_public = null;
	public int qualIndex;

	public String dumpMissingStuff() {
		StringBuilder results = new StringBuilder();
		results.append("================= Missing Types ===================\n");

		Set<TypeKey> missingTypes = new HashSet<TypeKey>(this.typesUsed);
		missingTypes.removeAll(this.typesDeclared);

		Set<MethodKey> missingMethods = new HashSet<MethodKey>(this.methodsUsed);
		missingMethods.removeAll(this.methodsDeclared);

		Set<FieldKey> missingFields = new HashSet<FieldKey>(this.fieldsUsed);
		missingFields.removeAll(this.fieldsDeclared);

		for (TypeKey t : missingTypes) {
			results.append("TYPE:" + t.baseTypeToString() + "\n");
		}

		for (MethodKey m : missingMethods) {
			results.append("METH:" + m + "\n");
		}

		for (FieldKey f : missingFields) {
			results.append("FIELD:" + f + " " + f.type + "\n");
		}

		results.append("=====================================================");
		return results.toString();
	}

	public String dumpMissingMethods() {
		StringBuilder results = new StringBuilder();
		Set<MethodKey> missingMethods = new HashSet<MethodKey>(this.methodsUsed);
		missingMethods.removeAll(this.methodsDeclared);
		for (MethodKey m : missingMethods) {
			results.append(m + "\n");
		}
		return results.toString();
	}

	public String dumpMissingFields() {
		StringBuilder results = new StringBuilder();
		Set<FieldKey> missingFields = new HashSet<FieldKey>(this.fieldsUsed);
		missingFields.removeAll(this.fieldsDeclared);
		for (FieldKey f : missingFields) {
			results.append(f + "\n");
		}
		return results.toString();
	}

	public void makeConservativeAssumptionsForMissingTypes() {
		Profile.logStart("*Make conservative assumptions for missing**");
		Set<TypeKey> missingTypes = new HashSet<TypeKey>(this.typesUsed);
		missingTypes.removeAll(this.typesDeclared);

		Set<MethodKey> missingMethods = new HashSet<MethodKey>(this.methodsUsed);
		missingMethods.removeAll(this.methodsDeclared);

		Set<FieldKey> missingFields = new HashSet<FieldKey>(this.fieldsUsed);
		missingFields.removeAll(this.fieldsDeclared);

		for (MethodKey m : missingMethods) {
			JqualPlugin.printlnLog("conservativeMethods", m.toString());
		}

		Profile.logEnd();
	}

	public String typesinfo() {
		StringBuilder results = new StringBuilder();
		results.append("\ndecl Types:\n==============\n");
		for (TypeKey t : this.typesDeclared) {
			results.append(t + "\n");
		}
		results.append("\ndecl Methods:\n================\n");
		for (MethodKey m : this.methodsDeclared) {
			results.append(m + "\n");
		}
		results.append("\ndecl Fields:\n===============\n");
		for (FieldKey f : this.fieldsDeclared) {
			results.append(f + "\n");
		}
		results.append("=====================================================");
		return results.toString();
	}

	public int ffiNumPotentialAnnotations() {
		int ret = 0;
		JqualPlugin.out.println("NATIVE COUNT: " + this.nativeMethods.size());
		for (MethodQType mqt : this.nativeMethods.values()) {
			ret += mqt.getFFIPositions();
		}

		return ret;
	}

	public void addClassDeclaration(TypeKey key, QType qtype) {
		this.declarations.add(new Declaration(key.toString(), qtype));
		if (qtype.original)
			this.numOriginalClasses += 1;
	}

	public void addMethodDeclaration(MethodKey key, QType qtype) {
		this.declarations.add(new Declaration(key.toString(), qtype));
		if (qtype.original)
			this.numOriginalMethods += 1;
	}

	public void addVariableDeclaration(String key, QType qtype) {
		this.declarations.add(new Declaration(key, qtype));
		if (qtype.original)
			this.numOriginalVars += 1;
	}

	public String declarationsToStringWithQuals() {
		StringBuilder ret = new StringBuilder();
		for (Declaration d : this.declarations) {
			if (d.original)
				ret.append(d.toStringWithQuals() + "\n\n");
		}
		return ret.toString();
	}

	public String methodDeclarationsToStringWithQuals() {
		StringBuilder ret = new StringBuilder();
		for (MethodQType mqt : getOriginalMethodQTypes()) {
			ret.append(mqt.getName());
			ret.append(mqt.toStringWithQuals(0) + "\n\n");
		}
		return ret.toString();
	}

	public List<MethodQType> getOriginalMethodQTypes() {

		List ret = new Vector();
		for (Declaration d : this.declarations) {
			if (((d.qtype instanceof MethodQType)) && (d.qtype.original)) {
				ret.add((MethodQType) d.qtype);
			}
		}
		return ret;
	}

	public JavariResults getJavariResults() {
		int numMethodPositions = 0;
		int numMethodPositionsRO = 0;
		int numFields = 0;
		int numFieldsFinal = 0;

		if (!JqualPlugin.inferReadonly) {
			return null;
		}
		if (this.javariResults == null) {
			for (MethodQType mqt : getOriginalMethodQTypes()) {
				numMethodPositions += mqt.getReadonlyPositions();
				numMethodPositionsRO += mqt.getReadonlyInferred();
			}

			for (ObjectQType o : this.objectQTypes) {
				if (o.original) {
					for (RefQType f : o.getFieldQTypes().values()) {
						numFields++;
						if (f.getQual().isReadonly()) {
							numFieldsFinal++;
						}
					}
				}
			}
			for (ObjectQType o : this.classQTypeMap.values()) {
				if (o.original) {
					for (RefQType f : o.getFieldQTypes().values()) {
						numFields++;

						if (f.getQual().isReadonly()) {
							numFieldsFinal++;
						}
					}
				}
			}
			this.javariResults = new JavariResults(numMethodPositions,
					numMethodPositionsRO, numFields, numFieldsFinal);
		}
		return this.javariResults;
	}

	public Qualifier getQualifierConstant(String name) {
		return (Qualifier) this.constants.get(name);
	}

	public Object putQualifierConstant(String name, Qualifier q) {
		return this.constants.put(name, q);
	}

	public String toString() {
		return this.results;
	}

	public void addQType(Object key, QType qt) {
		if ((qt instanceof ClassQType)) {
			throw new IllegalArgumentException(
					"Should be using addClassQType()");
		}
		if (qt == null) {
			throw new IllegalArgumentException("Passed null qtype for " + key);
		}
		if (this.qTypeMap.containsKey(key)) {
			QType old = (QType) this.qTypeMap.get(key);
			throw new IllegalArgumentException(
					"Duplicate key passed to addQType: " + key + "\nOld: "
							+ old.l + "\nnew: " + qt.l);
		}
		this.qTypeMap.put(key, qt);
	}

	public QType lookupQType(Object key) {
		QType ret = (QType) this.qTypeMap.get(key);
		if ((ret != null) && ((ret instanceof ClassQType)))
			throw new IllegalArgumentException(
					"Should be using lookupClassQType()");
		return ret;
	}

	public void addClassQType(TypeKey key, ClassQType qt) {
		if (qt == null) {
			throw new IllegalArgumentException("Passed null qtype for " + key);
		}

		this.classQTypeMap.put(key, qt);
	}

	public ClassQType lookupClassQType(TypeKey key) {
		return (ClassQType) this.classQTypeMap.get(key);
	}

	public String dumpQTypes() {
		StringBuffer results = new StringBuffer();
		results.append("=================QTypes Discovered===================\n");
		Iterator i = this.qTypeMap.entrySet().iterator();
		while (i.hasNext()) {
			Map.Entry e = (Map.Entry) (Map.Entry) i.next();

			results.append(e.getKey() + "\n");
			if ((e.getValue() instanceof MethodQType)) {
				MethodQType m = (MethodQType) e.getValue();
				results.append("  " + m.getReturnQType() + "\n");
				results.append("  " + m.getThisQType() + "\n");
				for (Iterator j = m.getParameterQTypes().iterator(); j
						.hasNext();) {
					results.append("  " + j.next() + "\n");
				}
			}
		}
		results.append("=====================================================");
		return results.toString();
	}

	public String dumpQualifiers() {
		StringBuffer ret = new StringBuffer();
		for (Iterator i = this.qualifiers.values().iterator(); i.hasNext();) {
			Qualifier q = (Qualifier) i.next();

			String inferred = q.getInferred();
			if (inferred != null) {
				ret.append(q + ":" + inferred);
				if ((!inferred.contains("mutable"))
						&& (!inferred.contains("readonly"))) {
					ret.append("<readonly> ");
				}
				ret.append("\n");
			} else if (JqualPlugin.showEmptyQuals) {
				ret.append(q + "\n");
			}
		}
		return ret.toString();
	}

	public void markSeen(ICompilationUnit c) {
		this.typesSeen.add(JqualPlugin.getName(c));
	}

	public void markSeen(ITypeBinding t) {
		this.typesSeen.add(t.getKey());
	}

	public boolean seen(ICompilationUnit c) {
		return this.typesSeen.contains(JqualPlugin.getName(c));
	}

	public boolean seen(ITypeBinding t) {
		return this.typesSeen.contains(t.getKey());
	}

	public void addToVisitList(ICompilationUnit c) {
		if (!seen(c)) {
			this.typesToVisit.push(c);
			markSeen(c);
		}
	}

	public boolean typesLeftToVisit() {
		return !this.typesToVisit.isEmpty();
	}

	public ICompilationUnit nextTypeToVisit() {
		return (ICompilationUnit) this.typesToVisit.pop();
	}

	public String dumpTypes() {
		StringBuffer ret = new StringBuffer();
		ret.append("================= Types found ===================\n");
		for (Iterator i = this.typesSeen.iterator(); i.hasNext();) {
			ret.append((String) i.next() + "\n");
		}
		ret.append("=================================================\n");
		return ret.toString();
	}

	public String createName(IBinding b) {
		String name = null;
		if (JqualPlugin.useLongNames)
			name = b.getKey();
		else {
			name = b.getName();
		}
		return name;
	}

	public void logMissingClass(String name, Location l) {
		JqualPlugin.printlnLog("missingClassLog", "Unknown class " + name
				+ " at " + l);
	}

	public boolean mutable(FieldKey key) {
		return this.mutableSet.contains(key);
	}

	public void setMutable(FieldKey key) {
		this.mutableSet.add(key);
	}

	public void setQualifier(Location l, Qualifier cq) {
		this.locationQualifiers.put(l, cq);
	}

	public Qualifier getQualifier(Location l) {
		return (Qualifier) this.locationQualifiers.get(l);
	}

	public Qualifier getQualifier(int nativeIndex) {
		return (Qualifier) this.qualifiers.get(new Integer(nativeIndex));
	}

	public void addQualifier(Qualifier q) {
		this.qualifiers.put(new Integer(q.getNativeIndex()), q);
	}

	public Location getLocation(int nativeIndex) {
		return (Location) this.locations.get(new Integer(nativeIndex));
	}

	public Location addLocation(Location loc) {
		return (Location) this.locations.put(new Integer(loc.nativeIndex), loc);
	}

	ClassQType getClassQType(ITypeBinding t) {
		return getClassQType(TypeKey.getTypeKey(t));
	}

	ClassQType getClassQType(TypeKey typekey) {
		if (typekey == null) {
			throw new NullPointerException();
		}

		ClassQType qt = lookupClassQType(typekey);

		String name = typekey.toString();

		name = name.toUpperCase();

		if (qt == null) {
			Profile.logMemStart("getClassQType/new Location");
			Location loc = new Location("Loc for CQT of " + typekey, 0L, 0L);
			Profile.logMemEnd();
			Profile.logMemStart("getClassQType/new ClassQType");
			qt = new ClassQType(typekey, loc, name, false);
			Profile.logMemEnd();
			addClassQType(typekey, qt);
		}

		return qt;
	}

	public String dumpObjects() {
		StringBuffer results = new StringBuffer();
		results.append("=================ObjectQTypes===================\n");
		Iterator i = this.objectQTypes.iterator();
		while (i.hasNext()) {
			results.append(((ObjectQType) i.next()).dump());
			results.append("------------------------------------------------\n");
		}
		results.append("=====================================================");
		return results.toString();
	}

	public void propagateConstraints() {
		boolean showUpdates = false;

		System.currentTimeMillis();
		while ((!this.mergeWorklist.isEmpty())
				|| (!this.constraintWorklist.isEmpty())) {
			WorklistJob j = this.mergeWorklist.isEmpty() ? (WorklistJob) this.constraintWorklist
					.pop() : (WorklistJob) this.mergeWorklist.pop();

			if ((showUpdates) && (this.constraintWorklist.size() % 500 == 0)) {
				JqualPlugin.out.println("Worklist: "
						+ this.constraintWorklist.size() + " Memory usage: "
						+ Profile.memoryUsage() / 1024L + "K (Java), "
						+ Profile.procMemoryKB() + "K (Total)");
				Native.profile();
			}
			if (JqualPlugin.showContraintMsgs)
				JqualPlugin.out.println("APPLYING: " + j);
			j.apply();
		}
	}

	public void addTypeFields(ITypeBinding t) {
		TypeKey classTypeKey = TypeKey.getTypeKey(t);
		if (this.typeFieldsMap.containsKey(classTypeKey)) {
			return;
		}
		addFieldsToClassAndParents(null, t);
	}

	private Vector<FieldKey> addFieldsToClassAndParents(
			Vector<FieldKey> passedUp, ITypeBinding t) {
		Vector passUp;

		if (passedUp != null)
			passUp = new Vector(passedUp);
		else {
			passUp = new Vector();
		}
		Vector passDown = new Vector();

		TypeKey classTypeKey = TypeKey.getTypeKey(t);

		Set myLegalFields = (Set) this.typeFieldsMap.get(classTypeKey);
		if (myLegalFields == null) {
			myLegalFields = new HashSet();
			this.typeFieldsMap.put(classTypeKey, myLegalFields);
		}

		myLegalFields.addAll(passUp);

		IVariableBinding[] fields = t.getDeclaredFields();
		for (int i = 0; i < fields.length; i++) {
			Profile.logMemStart("addFieldsToClassAndParents/FieldKey");
			FieldKey fk = FieldKey.getFieldKey(fields[i]);
			Profile.logMemEnd();
			passDown.add(fk);
			passUp.add(fk);
		}

		ITypeBinding parent = t.getSuperclass();
		if (parent == null) {
			if ((t.isClass()) && (!t.getKey().equals("Ljava/lang/Object;"))) {
				throw new RuntimeException(
						"OBJECT_TYPE_STRING is broken. Object id name is no longer Ljava/lang/Object; it is now "
								+ t.getName());
			}
			return passDown;
		}

		Vector<ITypeBinding> parents = new Vector<ITypeBinding>();
		parents.add(parent);
		ITypeBinding[] interfaces = t.getInterfaces();
		for (int i = 0; i < interfaces.length; i++) {
			parents.add(interfaces[i]);
		}

		if ((t.isNested()) && ((t.getModifiers() & 0x8) == 0)) {
			parents.add(t.getDeclaringClass());
		}

		for (ITypeBinding p : parents) {
			Vector res = addFieldsToClassAndParents(passUp, p);
			if (res != null) {
				passDown.addAll(res);
			}
		}
		myLegalFields.addAll(passDown);

		return passDown;
	}

	public String dumpLegalFields() {
		StringBuffer results = new StringBuffer();
		results.append("=================Type Fields Discovered===================\n");
		for (Map.Entry e : this.typeFieldsMap.entrySet()) {
			results.append(e.getKey() + "\n");
			Set<FieldKey> fields = (Set) e.getValue();
			for (FieldKey key : fields) {
				results.append("  " + key + "\n");
			}
			results.append("\n");
		}
		return results.toString();
	}

	public boolean isLegalField(TypeKey classType, FieldKey fieldKey) {
		if (!JqualPlugin.limitFields) {
			return true;
		}

		if (((fieldKey instanceof ArrayFieldKey))
				&& (classType == ObjectQType.OBJECT_TYPE_KEY)) {
			return true;
		}

		Set legalFields = (Set) this.typeFieldsMap.get(classType);

		return (legalFields != null) && (legalFields.contains(fieldKey));
	}

	public Vector<FieldQSig> getFieldQSigs() {
		Vector ret = new Vector();

		for (ObjectQType o : this.classQTypeMap.values()) {
			if (o.original) {
				for (RefQType f : o.getFieldQTypes().values()) {
					ret.add(new FieldQSig(f.getKey().declaringType.typeString
							+ "." + f.getKey().name, f.deref().getQual()
							.getInferred()));
				}
			}
		}
		return ret;
	}

	public Location getFieldLocation(String key) {
		Location ret = (Location) this.fieldLocations.get(key);
		if (ret == null) {
			Profile.logMemStart("getFieldLocation/new Location");
			ret = new Location("Field Location for " + key, 0L, 0L);
			Profile.logMemEnd();
		}
		return ret;
	}

	public Location getObjectFieldNodeLocation(String key) {
		Location ret = (Location) this.objectFieldNodeLocations.get(key);
		if (ret == null) {
			Profile.logMemStart("getObjectFieldNodeLocation/new Location");
			ret = new Location("Object Field Node Location for " + key, 0L, 0L);
			Profile.logMemEnd();
		}
		return ret;
	}

	public void initQuals() {
		this.qualIndex = 0;

		if (JqualPlugin.inferReadonly) {
			this.mutable = Qualifier.findQualifierConstant("mutable");
			if (this.mutable == null) {
				throw new RuntimeException(
						"inferReadonly is true but cannot find qualifier \"mutable\"");
			}
			this.readonly = Qualifier.findQualifierConstant("readonly");
			if (this.readonly == null) {
				throw new RuntimeException(
						"inferReadonly is true but cannot find qualifier \"readonly\"");
			}
		}

		if (JqualPlugin.inferOpaque) {
			this.transparent = Qualifier.findQualifierConstant("transparent");
			if (this.transparent == null) {
				throw new RuntimeException(
						"inferOpaque is true but cannot find qualifier \"transparent\"");
			}

			this.qual_public = this.transparent;
		}

		if (JqualPlugin.inferReadonly) {
			this.gateBlockJavari = new QualGate(true, true);
			this.gateBlockJavari.setAll(true);
			this.gateBlockJavari.addQual(this.mutable, false);
			this.gateBlockJavari.addQual(this.readonly, false);

			this.gateJavariOnly = new QualGate(true, true);
			this.gateJavariOnly.setAll(false);
			this.gateJavariOnly.addQual(this.mutable, true);
			this.gateJavariOnly.addQual(this.readonly, true);

			this.gateJavariBackwardOnly = new QualGate(false, true);
			this.gateJavariBackwardOnly.setAll(false);
			this.gateJavariBackwardOnly.addQual(this.mutable, true);
			this.gateJavariBackwardOnly.addQual(this.readonly, true);

			this.gateForwardOnly = new QualGate(true, false);
			this.gateForwardOnly.setAll(true);
		}

		if (JqualPlugin.inferInterned) {
			this.gateInternedOnly = new QualGate(true, true);
			this.gateInternedOnly.setAll(false);
			this.gateInternedOnly.addQual(
					Qualifier.findQualifierConstant("interned"), true);
			this.gateInternedOnly.addQual(
					Qualifier.findQualifierConstant("noninterned"), true);
		}
	}

	public class JavariResults {
		public int numMethodPositions;
		public int numMethodPositionsRO;
		public int numFields;
		public int numFieldsFinal;

		public JavariResults(int numMethodPositions, int numMethodPositionsRO,
				int numFields, int numFieldsFinal) {
			this.numMethodPositions = numMethodPositions;
			this.numMethodPositionsRO = numMethodPositionsRO;
			this.numFields = numFields;
			this.numFieldsFinal = numFieldsFinal;
		}
	}

	static class Declaration implements Comparable {
		String key;
		boolean original;
		QType qtype;

		public Declaration(String key, QType qtype) {
			this.key = key;
			this.qtype = qtype;
			this.original = qtype.original;
		}

		public int compareTo(Object o) {
			if (!(o instanceof Declaration))
				throw new UnsupportedOperationException("why compare " + o
						+ " with " + this.key + "?");
			return this.key.compareTo(((Declaration) o).key);
		}

		public String toStringWithQuals() {
			return this.key + ":" + this.qtype.toStringWithQuals(0);
		}

		public int hashCode() {
			int result = 1;
			result = 31 * result + (this.key == null ? 0 : this.key.hashCode());
			return result;
		}

		public boolean equals(Object obj) {
			if (this == obj)
				return true;
			if (obj == null)
				return false;
			if (getClass() != obj.getClass())
				return false;
			Declaration other = (Declaration) obj;
			if (this.key == null) {
				if (other.key != null)
					return false;
			} else if (!this.key.equals(other.key))
				return false;
			return true;
		}
	}
}
